1  /-
  2  Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Zhouhang Zhou
  5  -/
  6  
  7  import analysis.convex.basic algebra.quadratic_discriminant analysis.complex.exponential
src         └───────────────────┘ └────────────────────────────┘ └──────────────────────────┘
  8         analysis.specific_limits
src         └──────────────────────┘
  9  import tactic.monotonicity
src         └─────────────────┘
 10  
 11  
 12  /-!
 13  # Inner Product Space
 14  
 15  This file defines real inner product space and proves its basic properties.
 16  
 17  An inner product space is a vector space endowed with an inner product. It generalizes the notion of
 18  dot product in `ℝ^n` and provides the means of defining the length of a vector and the angle between
 19  two vectors. In particular vectors `x` and `y` are orthogonal if their inner product equals zero.
 20  
 21  ## Main statements
 22  
 23  Existence of orthogonal projection onto nonempty complete subspace:
 24  Let `u` be a point in an inner product space, and let `K` be a nonempty complete subspace.
 25  Then there exists a unique `v` in `K` that minimizes the distance `∥u - v∥` to `u`.
 26  The point `v` is usually called the orthogonal projection of `u` onto `K`.
 27  
 28  ## Implementation notes
 29  
 30  We decide to develop the theory of real inner product spaces and that of complex inner product
 31  spaces separately.
 32  
 33  ## Tags
 34  
 35  inner product space, norm, orthogonal projection
 36  
 37  ## References
 38  *  [Clément & Martin, *The Lax-Milgram Theorem. A detailed proof to be formalized in Coq*]
 39  *  [Clément & Martin, *A Coq formal proof of the Lax–Milgram theorem*]
 40  
 41  The Coq code is available at the following address: <http://www.lri.fr/~sboldo/elfic/index.html>
 42  -/
 43  
 44  noncomputable theory
 45  
 46  open real set lattice
 47  open_locale topological_space
 48  
 49  universes u v w
 50  
 51  variables {α : Type u} {F : Type v} {G : Type w}
 52  
 53  set_option class.instance_max_depth 40
doc             └──────────────────────┘
 54  
 55  class has_inner (α : Type*) := (inner : α → α → ℝ)
id                        └───┘                   
src                                                  
typ                       └───┘                   
 56  
 57  export has_inner (inner)
 58  
 59  section prio
 60  set_option default_priority 100 -- see Note [default priority]
doc             └──────────────┘
 61  -- see Note[vector space definition] for why we extend `module`.
 62  /--
 63  An inner product space is a real vector space with an additional operation called inner product.
 64  Inner product spaces over complex vector space will be defined in another file.
 65  -/
 66  class inner_product_space (α : Type*) extends add_comm_group α, module ℝ α, has_inner α :=
 67  (comm      : ∀ x y, inner x y = inner y x)
 68  (nonneg    : ∀ x, 0 ≤ inner x x)
 69  (definite  : ∀ x, inner x x = 0 → x = 0)
 70  (add_left  : ∀ x y z, inner (x + y) z = inner x z + inner y z)
 71  (smul_left : ∀ x y r, inner (r • x) y = r * inner x y)
 72  end prio
 73  
 74  variable [inner_product_space α]
id             └─────────────────┘
src            └─────────────────┘
typ            └─────────────────┘
doc            └─────────────────┘
 75  
 76  section basic_properties
 77  
 78  lemma inner_comm (x y : α) : inner x y = inner y x := inner_product_space.comm x y
id                               └───┘    └───┘      └──────────────────────┘  
src                               └───┘      └───┘        └──────────────────────┘
typ                              └───┘    └───┘      └──────────────────────┘  
 79  
 80  lemma inner_self_nonneg {x : α} : 0 ≤ inner x x := inner_product_space.nonneg _
id                                       └───┘      └────────────────────────┘
src                                       └───┘        └────────────────────────┘
typ                                      └───┘      └────────────────────────┘
 81  
 82  lemma inner_add_left {x y z : α} : inner (x + y) z = inner x z + inner y z :=
id                                     └───┘        └───┘    └───┘  
src                                     └───┘           └───┘      └───┘
typ                                    └───┘        └───┘    └───┘  
 83  inner_product_space.add_left _ _ _
id   └──────────────────────────┘
src  └──────────────────────────┘
typ  └──────────────────────────┘
 84  
 85  lemma inner_add_right {x y z : α} : inner x (y + z) = inner x y + inner x z :=
id                                      └───┘        └───┘    └───┘  
src                                      └───┘           └───┘      └───┘
typ                                     └───┘        └───┘    └───┘  
 86  by { rw [inner_comm, inner_add_left], simp [inner_comm] }
id            └────────┘  └────────────┘         └────────┘
src       └──┘└────────┘└┘└────────────┘  └────┘└────────┘└┘
typ       └──┘└────────┘└┘└────────────┘  └────┘└────────┘└┘
doc       └──┘          └┘                └────┘          └┘
txt       └──┘          └┘                └────┘          └┘
par       └──┘          └┘                └────┘          └┘
pid         └┘          └┘                              
st     └───────────────┘└──────────────┘└───────────────────┘└┘
 87  
 88  lemma inner_smul_left {x y : α} {r : ℝ} : inner (r • x) y = r * inner x y :=
id                                           └───┘          └───┘  
src                                           └───┘              └───┘
typ                                          └───┘          └───┘  
 89  inner_product_space.smul_left _ _ _
id   └───────────────────────────┘
src  └───────────────────────────┘
typ  └───────────────────────────┘
 90  
 91  lemma inner_smul_right {x y : α} {r : ℝ} : inner x (r • y) = r * inner x y :=
id                                            └───┘          └───┘  
src                                            └───┘              └───┘
typ                                           └───┘          └───┘  
 92  by { rw [inner_comm, inner_smul_left, inner_comm] }
id            └────────┘  └─────────────┘  └────────┘
src       └──┘└────────┘└┘└─────────────┘└┘└────────┘└┘
typ       └──┘└────────┘└┘└─────────────┘└┘└────────┘└┘
doc       └──┘          └┘               └┘          └┘
txt       └──┘          └┘               └┘          └┘
par       └──┘          └┘               └┘          └┘
pid         └┘          └┘               └┘          
st     └───────────────┘└───────────────┘└──────────┘└┘
 93  
 94  @[simp] lemma inner_zero_left {x : α} : inner 0 x = 0 :=
id                                          └───┘    
src                                          └───┘     
typ                                         └───┘    
doc    └──┘
 95  by { rw [← zero_smul ℝ (0:α), inner_smul_left, zero_mul] }
id              └───────┘         └─────────────┘  └──────┘
src       └────┘└───────┘  └┘ └─┘└─────────────┘└┘└──────┘└┘
typ       └────┘└───────┘  └┘└─┘└─────────────┘└┘└──────┘└┘
doc       └────┘           └┘ └─┘               └┘        └┘
txt       └────┘           └┘ └─┘               └┘        └┘
par       └────┘           └┘ └─┘               └┘        └┘
pid         └──┘           └┘ └─┘               └┘        
st     └────────────────────────┘└───────────────┘└────────┘└┘
 96  
 97  @[simp] lemma inner_zero_right {x : α} : inner x 0 = 0 :=
id                                           └───┘    
src                                           └───┘     
typ                                          └───┘    
doc    └──┘
 98  by { rw [inner_comm, inner_zero_left] }
id            └────────┘  └─────────────┘
src       └──┘└────────┘└┘└─────────────┘└┘
typ       └──┘└────────┘└┘└─────────────┘└┘
doc       └──┘          └┘               └┘
txt       └──┘          └┘               └┘
par       └──┘          └┘               └┘
pid         └┘          └┘               
st     └───────────────┘└───────────────┘└┘
 99  
100  lemma inner_self_eq_zero (x : α) : inner x x = 0 ↔ x = 0 :=
id                                     └───┘        
src                                     └───┘           
typ                                    └───┘        
101  iff.intro (inner_product_space.definite _) (by { rintro rfl, exact inner_zero_left })
id   └───────┘  └──────────────────────────┘                            └─────────────┘
src  └───────┘  └──────────────────────────┘          └────────┘  └────┘└─────────────┘
typ  └───────┘  └──────────────────────────┘          └────────┘  └────┘└─────────────┘
doc                                                   └────────┘  └────┘               
txt                                                   └────────┘  └────┘               
par                                                   └────────┘  └────┘               
pid                                                         └──┘                      
st                                                 └───────────┘└──────────────────────┘└┘
102  
103  @[simp] lemma inner_neg_left {x y : α} : inner (-x) y = -inner x y :=
id                                           └───┘      └───┘  
src                                           └───┘        └───┘
typ                                          └───┘      └───┘  
doc    └──┘
104  by { rw [← neg_one_smul ℝ x, inner_smul_left], simp }
id              └──────────┘     └─────────────┘
src       └────┘└──────────┘  └┘└─────────────┘  └───┘
typ       └────┘└──────────┘ └┘└─────────────┘  └───┘
doc       └────┘              └┘                 └───┘
txt       └────┘              └┘                 └───┘
par       └────┘              └┘                 └───┘
pid         └──┘              └┘                     
st     └───────────────────────┘└───────────────┘└──────┘└┘
105  
106  @[simp] lemma inner_neg_right {x y : α} : inner x (-y) = -inner x y :=
id                                            └───┘      └───┘  
src                                            └───┘        └───┘
typ                                           └───┘      └───┘  
doc    └──┘
107  by { rw [inner_comm, inner_neg_left, inner_comm] }
id            └────────┘  └────────────┘  └────────┘
src       └──┘└────────┘└┘└────────────┘└┘└────────┘└┘
typ       └──┘└────────┘└┘└────────────┘└┘└────────┘└┘
doc       └──┘          └┘              └┘          └┘
txt       └──┘          └┘              └┘          └┘
par       └──┘          └┘              └┘          └┘
pid         └┘          └┘              └┘          
st     └───────────────┘└──────────────┘└──────────┘└┘
108  
109  @[simp] lemma inner_neg_neg {x y : α} : inner (-x) (-y) = inner x y := by simp
id                                          └───┘        └───┘  
src                                          └───┘          └───┘           └────
typ                                         └───┘        └───┘         └────
doc    └──┘                                                                    └────
txt                                                                            └────
par                                                                            └────
pid                                                                                
st                                                                            └─────
110  
src  
typ  
doc  
txt  
par  
pid  
st   
111  lemma inner_sub_left {x y z : α} : inner (x - y) z = inner x z - inner y z :=
id                                     └───┘        └───┘    └───┘  
src                                     └───┘           └───┘      └───┘
typ                                    └───┘        └───┘    └───┘  
112  by { simp [sub_eq_add_neg, inner_add_left] }
id              └────────────┘  └────────────┘
src       └────┘└────────────┘└┘└────────────┘└┘
typ       └────┘└────────────┘└┘└────────────┘└┘
doc       └────┘              └┘              └┘
txt       └────┘              └┘              └┘
par       └────┘              └┘              └┘
pid                         └┘              
st     └───────────────────────────────────────┘└┘
113  
114  lemma inner_sub_right {x y z : α} : inner x (y - z) = inner x y - inner x z :=
id                                      └───┘        └───┘    └───┘  
src                                      └───┘           └───┘      └───┘
typ                                     └───┘        └───┘    └───┘  
115  by { simp [sub_eq_add_neg, inner_add_right] }
id              └────────────┘  └─────────────┘
src       └────┘└────────────┘└┘└─────────────┘└┘
typ       └────┘└────────────┘└┘└─────────────┘└┘
doc       └────┘              └┘               └┘
txt       └────┘              └┘               └┘
par       └────┘              └┘               └┘
pid                         └┘               
st     └────────────────────────────────────────┘└┘
116  
117  /-- Expand `inner (x + y) (x + y)` -/
118  lemma inner_add_add_self {x y : α} : inner (x + y) (x + y) = inner x x + 2 * inner x y + inner y y :=
id                                       └───┘            └───┘       └───┘    └───┘  
src                                       └───┘                └───┘         └───┘      └───┘
typ                                      └───┘            └───┘       └───┘    └───┘  
119  by { simpa [inner_add_left, inner_add_right, two_mul] using inner_comm _ _ }
id               └────────────┘  └─────────────┘  └─────┘        └────────┘
src       └─────┘└────────────┘└┘└─────────────┘└┘└─────┘└──────┘└────────┘└───┘
typ       └─────┘└────────────┘└┘└─────────────┘└┘└─────┘└──────┘└────────┘└───┘
doc       └─────┘              └┘               └┘       └──────┘          └───┘
txt       └─────┘              └┘               └┘       └──────┘          └───┘
par       └─────┘              └┘               └┘       └──────┘          └───┘
pid                          └┘               └┘       └────┘          └──┘
st     └───────────────────────────────────────────────────────────────────────┘└┘
120  
121  /-- Expand `inner (x - y) (x - y)` -/
122  lemma inner_sub_sub_self {x y : α} : inner (x - y) (x - y) = inner x x - 2 * inner x y + inner y y :=
id                                       └───┘            └───┘       └───┘    └───┘  
src                                       └───┘                └───┘         └───┘      └───┘
typ                                      └───┘            └───┘       └───┘    └───┘  
123  by { simp only [inner_sub_left, inner_sub_right, two_mul], simpa using inner_comm _ _ }
id                   └────────────┘  └─────────────┘  └─────┘               └────────┘
src       └─────────┘└────────────┘└┘└─────────────┘└┘└─────┘  └──────────┘└────────┘└───┘
typ       └─────────┘└────────────┘└┘└─────────────┘└┘└─────┘  └──────────┘└────────┘└───┘
doc       └─────────┘              └┘               └┘         └──────────┘          └───┘
txt       └─────────┘              └┘               └┘         └──────────┘          └───┘
par       └─────────┘              └┘               └┘         └──────────┘          └───┘
pid           └──┘└┘              └┘               └┘              └────┘          └──┘
st     └─────────────────────────────────────────────────────┘└───────────────────────────┘└┘
124  
125  /-- Parallelogram law -/
126  lemma parallelogram_law {x y : α} :
id                                  
typ                                 
127    inner (x + y) (x + y) + inner (x - y) (x - y) = 2 * (inner x x + inner y y) :=
id     └───┘            └───┘                └───┘    └───┘  
src    └───┘                └───┘                    └───┘      └───┘
typ    └───┘            └───┘                └───┘    └───┘  
128  by { simp [inner_add_add_self, inner_sub_sub_self, two_mul] }
id              └────────────────┘  └────────────────┘  └─────┘
src       └────┘└────────────────┘└┘└────────────────┘└┘└─────┘└┘
typ       └────┘└────────────────┘└┘└────────────────┘└┘└─────┘└┘
doc       └────┘└────────────────┘└┘└────────────────┘└┘       └┘
txt       └────┘                  └┘                  └┘       └┘
par       └────┘                  └┘                  └┘       └┘
pid                             └┘                  └┘       
st     └────────────────────────────────────────────────────────┘└┘
129  
130  /-- Cauchy–Schwarz inequality -/
131  lemma inner_mul_inner_self_le (x y : α) : inner x y * inner x y ≤ inner x x * inner y y :=
id                                            └───┘    └───┘    └───┘    └───┘  
src                                            └───┘      └───┘      └───┘      └───┘
typ                                           └───┘    └───┘    └───┘    └───┘  
132  begin
st   └─────
133    have : ∀ t, 0 ≤ inner y y * t * t + 2 * inner x y * t + inner x x, from
id                                                         └───┘   
src    └─────┘ └┘ └─┘          └─┘           └───┘    └────
typ    └─────┘ └┘ └─┘          └─┘          └───┘   └────
doc    └─────┘ └┘ └─┘             └─┘                    └────
txt    └─────┘ └┘ └─┘             └─┘                    └────
par    └─────┘ └┘ └─┘             └─┘                    └────
pid    └───┘└┘ └┘ └─┘             └─┘                    └────
st   ──────────────────────────────────────────────────────────────────┘└──────
134      assume t, calc
src  ───┘      └──┘    
typ  ───┘      └──┘    
doc  ───┘      └──┘    
txt  ───┘      └──┘    
par  ───┘      └──┘    
pid  ───┘      └──┘    
st   ───────────────────
135        0 ≤ inner (x+t•y) (x+t•y) : inner_self_nonneg
id                                    └───────────────┘
src  ───────┘           └┘      └──┘└───────────────┘
typ  ───────┘           └┘      └──┘└───────────────┘
doc  ───────┘            └┘      └──┘                 
txt  ───────┘            └┘      └──┘                 
par  ───────┘            └┘      └──┘                 
pid  ───────┘            └┘      └──┘                 
st   ────────────────────────────────────────────────────
136        ... = inner y y * t * t + 2 * inner x y * t + inner x x :
id                                                      └───┘   
src  ─────────┘             └─┘           └───┘  └──
typ  ─────────┘             └─┘          └───┘ └──
doc  ─────────┘             └─┘                  └──
txt  ─────────┘             └─┘                  └──
par  ─────────┘             └─┘                  └──
pid  ─────────┘             └─┘                  └──
st   ────────────────────────────────────────────────────────────────
137          by { simp only [inner_add_add_self, inner_smul_right, inner_smul_left], ring },
id                           └────────────────┘  └──────────────┘  └─────────────┘
src  ───────┘  └─┘└─────────┘└────────────────┘└┘└──────────────┘└┘└─────────────┘└┘└───┘
typ  ───────┘  └─┘└─────────┘└────────────────┘└┘└──────────────┘└┘└─────────────┘└┘└───┘
doc  ───────┘  └─┘└─────────┘└────────────────┘└┘                └┘               └┘└───┘
txt  ───────┘  └─┘└─────────┘                  └┘                └┘               └┘└───┘
par  ───────┘  └─┘└─────────┘                  └┘                └┘               └┘└───┘
pid  ───────┘  └────────────┘                  └┘                └┘               └───────┘
st   ─────────┘└──────────────────────────────────────────────────────────────────┘└─────┘└┘
138    have := discriminant_le_zero this, rw discrim at this,
id             └──────────────────┘ └──┘     └─────┘
src    └──────┘└──────────────────┘      └─┘└─────┘└──────┘
typ    └──────┘└──────────────────┘└──┘  └─┘└─────┘└──────┘
doc    └──────┘└──────────────────┘      └─┘└─────┘└──────┘
txt    └──────┘                          └─┘       └──────┘
par    └──────┘                          └─┘       └──────┘
pid    └───┘└─┘                                   └──────┘
st   ──────────────────────────────────┘└──────────────────┘└─
139    have h : (2 * inner x y)^2 - 4 * inner y y * inner x x =
id                                                          
src    └───────┘ └┘        └┘└─┘                
typ    └───────┘ └┘        └┘└─┘                
doc    └───────┘ └┘         └┘ └─┘                 
txt    └───────┘ └┘         └┘ └─┘                 
par    └───────┘ └┘         └┘ └─┘                 
pid    └────┘└─┘ └┘         └┘ └─┘                 
st   ───────────────────────────────────────────────────────────
140                        4 * (inner x y * inner x y - inner x x * inner y y) := by ring,
id                                                                 └───┘   
src  ───────────────────────┘                          └───┘  └───┘  └──┘
typ  ───────────────────────┘                         └───┘ └───┘  └──┘
doc  ───────────────────────┘                                 └───┘  └──┘
txt  ───────────────────────┘                                 └───┘  └──┘
par  ───────────────────────┘                                 └───┘  └──┘
pid  ───────────────────────┘                                 └──┘  └───┘
st   ──────────────────────────────────────────────────────────────────────────────┘└───┘└─
141    rw h at this,
id        
src    └─┘ └──────┘
typ    └─┘└──────┘
doc    └─┘ └──────┘
txt    └─┘ └──────┘
par    └─┘ └──────┘
pid       └──────┘
st   ─────────────┘└─
142    linarith
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
pid            
st   ──────────┘
143  end
st   └─┘
144  
145  end basic_properties
146  
147  section norm
148  
149  /-- An inner product naturally induces a norm. -/
150  @[priority 100] -- see Note [lower instance priority]
151  instance inner_product_space_has_norm : has_norm α := ⟨λx, sqrt (inner x x)⟩
id                                           └──────┘         └──┘  └───┘  
src                                          └──────┘           └──┘  └───┘
typ                                          └──────┘         └──┘  └───┘  
doc                                          └──────┘
152  
153  lemma norm_eq_sqrt_inner {x : α} : ∥x∥ = sqrt (inner x x) := rfl
id                                       └──┘  └───┘       └─┘
src                                        └──┘  └───┘         └─┘
typ                                      └──┘  └───┘       └─┘
154  
155  lemma inner_self_eq_norm_square (x : α) : inner x x = ∥x∥ * ∥x∥ := (mul_self_sqrt inner_self_nonneg).symm
id                                            └───┘           └───────────┘ └───────────────┘ └──┘
src                                            └───┘               └───────────┘ └───────────────┘ └──┘
typ                                           └───┘           └───────────┘ └───────────────┘ └──┘
156  
157  /-- Expand the square -/
158  lemma norm_add_pow_two {x y : α} : ∥x + y∥^2 = ∥x∥^2 + 2 * inner x y + ∥y∥^2 :=
id                                                └───┘    
src                                                   └───┘       
typ                                               └───┘    
159  by { repeat {rw [pow_two, ← inner_self_eq_norm_square]}, exact inner_add_add_self }
id                    └─────┘    └───────────────────────┘          └────────────────┘
src       └──────┘└──┘└─────┘└──┘└───────────────────────┘  └────┘└────────────────┘
typ       └──────┘└──┘└─────┘└──┘└───────────────────────┘  └────┘└────────────────┘
doc       └──────┘└──┘       └──┘                           └────┘└────────────────┘
txt       └──────┘└──┘       └──┘                           └────┘                  
par       └──────┘└──┘       └──┘                           └────┘                  
pid             └────┘       └──┘                         └┘                         
st     └────────────────────┘└───────────────────────────┘└─┘└────────────────────────┘└┘
160  
161  /-- Same lemma as above but in a different form -/
162  lemma norm_add_mul_self {x y : α} : ∥x + y∥ * ∥x + y∥ = ∥x∥ * ∥x∥ + 2 * inner x y + ∥y∥ * ∥y∥ :=
id                                                     └───┘      
src                                                           └───┘          
typ                                                    └───┘      
163  by { repeat {rw [← pow_two]}, exact norm_add_pow_two }
id                      └─────┘          └──────────────┘
src       └──────┘└────┘└─────┘  └────┘└──────────────┘
typ       └──────┘└────┘└─────┘  └────┘└──────────────┘
doc       └──────┘└────┘         └────┘└──────────────┘
txt       └──────┘└────┘         └────┘                
par       └──────┘└────┘         └────┘                
pid             └──────┘       └┘                       
st     └──────────────────────┘└─┘└──────────────────────┘└┘
164  
165  /-- Expand the square -/
166  lemma norm_sub_pow_two {x y : α} : ∥x - y∥^2 = ∥x∥^2 - 2 * inner x y + ∥y∥^2 :=
id                                                └───┘    
src                                                   └───┘       
typ                                               └───┘    
167  by { repeat {rw [pow_two, ← inner_self_eq_norm_square]}, exact inner_sub_sub_self }
id                    └─────┘    └───────────────────────┘          └────────────────┘
src       └──────┘└──┘└─────┘└──┘└───────────────────────┘  └────┘└────────────────┘
typ       └──────┘└──┘└─────┘└──┘└───────────────────────┘  └────┘└────────────────┘
doc       └──────┘└──┘       └──┘                           └────┘└────────────────┘
txt       └──────┘└──┘       └──┘                           └────┘                  
par       └──────┘└──┘       └──┘                           └────┘                  
pid             └────┘       └──┘                         └┘                         
st     └────────────────────┘└───────────────────────────┘└─┘└────────────────────────┘└┘
168  
169  /-- Same lemma as above but in a different form -/
170  lemma norm_sub_mul_self {x y : α} : ∥x - y∥ * ∥x - y∥ = ∥x∥ * ∥x∥ - 2 * inner x y + ∥y∥ * ∥y∥ :=
id                                                     └───┘      
src                                                           └───┘          
typ                                                    └───┘      
171  by { repeat {rw [← pow_two]}, exact norm_sub_pow_two }
id                      └─────┘          └──────────────┘
src       └──────┘└────┘└─────┘  └────┘└──────────────┘
typ       └──────┘└────┘└─────┘  └────┘└──────────────┘
doc       └──────┘└────┘         └────┘└──────────────┘
txt       └──────┘└────┘         └────┘                
par       └──────┘└────┘         └────┘                
pid             └──────┘       └┘                       
st     └──────────────────────┘└─┘└──────────────────────┘└┘
172  
173  /-- Cauchy–Schwarz inequality with norm -/
174  lemma abs_inner_le_norm (x y : α) : abs (inner x y) ≤ ∥x∥ * ∥y∥ :=
id                                      └─┘  └───┘       
src                                      └─┘  └───┘           
typ                                     └─┘  └───┘       
175  nonneg_le_nonneg_of_squares_le (mul_nonneg (sqrt_nonneg _) (sqrt_nonneg _))
id   └────────────────────────────┘  └────────┘  └─────────┘     └─────────┘
src  └────────────────────────────┘  └────────┘  └─────────┘     └─────────┘
typ  └────────────────────────────┘  └────────┘  └─────────┘     └─────────┘
176  begin
st   └─────
177    rw abs_mul_abs_self,
id        └──────────────┘
src    └─┘└──────────────┘
typ    └─┘└──────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────────────┘└─
178    have : ∥x∥ * ∥y∥ * (∥x∥ * ∥y∥) = inner x x * inner y y,
id                                             └───┘   
src    └─────┘             └┘        └───┘ 
typ    └─────┘             └┘       └───┘ 
doc    └─────┘                └┘               
txt    └─────┘                └┘               
par    └─────┘                └┘               
pid    └───┘└┘                └┘               
st   ───────────────────────────────────────────────────────┘└─
179      simp only [inner_self_eq_norm_square], ring,
id                  └───────────────────────┘
src      └─────────┘└───────────────────────┘  └──┘
typ      └─────────┘└───────────────────────┘  └──┘
doc      └─────────┘                           └──┘
txt      └─────────┘                           └──┘
par      └─────────┘                           └──┘
pid          └──┘└┘                         
st   ────────────────────────────────────────┘└────┘└─
180    rw this,
id        └──┘
src    └─┘
typ    └─┘└──┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────┘└─
181    exact inner_mul_inner_self_le _ _
id           └─────────────────────┘
src    └────┘└─────────────────────┘└───┘
typ    └────┘└─────────────────────┘└───┘
doc    └────┘└─────────────────────┘└───┘
txt    └────┘                       └───┘
par    └────┘                       └───┘
pid                                └──┘
st   ───────────────────────────────────┘
182  end
st   └─┘
183  
184  lemma parallelogram_law_with_norm {x y : α} :
id                                            
typ                                           
185    ∥x + y∥ * ∥x + y∥ + ∥x - y∥ * ∥x - y∥ = 2 * (∥x∥ * ∥x∥ + ∥y∥ * ∥y∥) :=
id                               
src                                          
typ                              
186  by { simp only [(inner_self_eq_norm_square _).symm], exact parallelogram_law }
id                    └───────────────────────┘                 └───────────────┘
src       └─────────┘ └───────────────────────┘└───────┘  └────┘└───────────────┘
typ       └─────────┘ └───────────────────────┘└───────┘  └────┘└───────────────┘
doc       └─────────┘                          └───────┘  └────┘└───────────────┘
txt       └─────────┘                          └───────┘  └────┘                 
par       └─────────┘                          └───────┘  └────┘                 
pid           └──┘└┘                          └───────┘                        
st     └───────────────────────────────────────────────┘└────────────────────────┘└┘
187  
188  /-- An inner product space forms a normed group w.r.t. its associated norm. -/
189  @[priority 100] -- see Note [lower instance priority]
190  instance inner_product_space_is_normed_group : normed_group α :=
id                                                  └──────────┘ 
src                                                 └──────────┘
typ                                                 └──────────┘ 
doc                                                 └──────────┘
191  normed_group.of_core α
id   └──────────────────┘ 
src  └──────────────────┘
typ  └──────────────────┘ 
doc  └──────────────────┘
192  { norm_eq_zero_iff := assume x, iff.intro
id                                  └───────┘
src                                  └───────┘
typ                                 └───────┘
193      (λ h : sqrt (inner x x) = 0, (inner_self_eq_zero x).1 $ (sqrt_eq_zero inner_self_nonneg).1 h )
id              └──┘  └───┘         └────────────────┘       └──────────┘ └───────────────┘   
src             └──┘  └───┘           └────────────────┘        └──────────┘ └───────────────┘ 
typ             └──┘  └───┘         └────────────────┘       └──────────┘ └───────────────┘   
194      (by {rintro rfl, show sqrt (inner (0:α) 0) = 0, simp }),
id                             └──┘  └───┘         
src           └────────┘  └───┘└──┘ └───┘ └┘ └───┘└┘  └───┘
typ           └────────┘  └───┘└──┘ └───┘ └┘└───┘└┘  └───┘
doc           └────────┘  └───┘           └┘ └───┘ └┘  └───┘
txt           └────────┘  └───┘           └┘ └───┘ └┘  └───┘
par           └────────┘  └───┘           └┘ └───┘ └┘  └───┘
pid                 └──┘  └───┘           └┘ └───┘       
st          └──────────┘└─────────────────────────────┘└─────┘└┘
195    triangle := assume x y,
id                         
typ                        
196    begin
st     └─────
197      have := calc
src      └──────┘    
typ      └──────┘    
doc      └──────┘    
txt      └──────┘    
par      └──────┘    
pid      └───┘└─┘    
st   ─────────────────
198        ∥x + y∥ * ∥x + y∥ = inner (x + y) (x + y) : (inner_self_eq_norm_square _).symm
id                         └───┘                  └───────────────────────┘
src  ─────┘        └───┘    └┘    └──┘ └───────────────────────┘└────────
typ  ─────┘        └───┘    └┘  └──┘ └───────────────────────┘└────────
doc  ─────┘                     └┘    └──┘                          └────────
txt  ─────┘                     └┘    └──┘                          └────────
par  ─────┘                     └┘    └──┘                          └────────
pid  ─────┘                     └┘    └──┘                          └────────
st   ─────────────────────────────────────────────────────────────────────────────────────
199        ... = inner x x + 2 * inner x y + inner y y : inner_add_add_self
id                                                       └────────────────┘
src  ─────────┘         └─┘                └─┘└────────────────┘
typ  ─────────┘         └─┘                └─┘└────────────────┘
doc  ─────────┘         └─┘                └─┘└────────────────┘
txt  ─────────┘         └─┘                └─┘                  
par  ─────────┘         └─┘                └─┘                  
pid  ─────────┘         └─┘                └─┘                  
st   ───────────────────────────────────────────────────────────────────────
200        ... ≤ inner x x + 2 * (∥x∥ * ∥y∥) + inner y y :
src  ─────────┘         └─┘         └┘        └──
typ  ─────────┘         └─┘         └┘        └──
doc  ─────────┘         └─┘         └┘        └──
txt  ─────────┘         └─┘         └┘        └──
par  ─────────┘         └─┘         └┘        └──
pid  ─────────┘         └─┘         └┘        └──
st   ──────────────────────────────────────────────────────
201          by linarith [abs_inner_le_norm x y, le_abs_self (inner x y)]
id                        └───────────────┘    └─────────┘  └───┘  
src  ───────┘  └────────┘└───────────────┘  └┘└─────────┘ └───┘  └──
typ  ───────┘  └────────┘└───────────────┘└┘└─────────┘ └───┘└──
doc  ───────┘  └────────┘└───────────────┘  └┘                   └──
txt  ───────┘  └────────┘                   └┘                   └──
par  ───────┘  └────────┘                   └┘                   └──
pid  ───────┘  └─────────┘                   └┘                   └──
st   ─────────┘└──────────────────────────────────────────────────────────
202        ... = (∥x∥ + ∥y∥) * (∥x∥ + ∥y∥) : by { simp only [inner_self_eq_norm_square], ring },
id                                                           └───────────────────────┘
src  ─────┘└──┘         └┘         └──┘  └─┘└─────────┘└───────────────────────┘└┘└───┘
typ  ─────┘└──┘         └┘         └──┘  └─┘└─────────┘└───────────────────────┘└┘└───┘
doc  ─────┘└──┘         └┘         └──┘  └─┘└─────────┘                         └┘└───┘
txt  ─────┘└──┘         └┘         └──┘  └─┘└─────────┘                         └┘└───┘
par  ─────┘└──┘         └┘         └──┘  └─┘└─────────┘                         └┘└───┘
pid  ─────────┘         └┘         └──┘  └────────────┘                         └───────┘
st   ─────┘└──────────────────────────────────┘└──────────────────────────────────────┘└─────┘└┘
203      exact nonneg_le_nonneg_of_squares_le (add_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) this
id             └────────────────────────────┘  └────────┘                  └─────────┘     └──┘
src      └────┘└────────────────────────────┘ └────────┘            └──┘ └─────────┘└───┘    
typ      └────┘└────────────────────────────┘ └────────┘            └──┘ └─────────┘└───┘└──┘
doc      └────┘                                                     └──┘            └───┘    
txt      └────┘                                                     └──┘            └───┘    
par      └────┘                                                     └──┘            └───┘    
pid                                                                └──┘            └───┘    
st   ───────────────────────────────────────────────────────────────────────────────────────────
204    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
205    norm_neg := λx, show sqrt (inner (-x) (-x)) = sqrt (inner x x), by simp }
id                         └──┘  └───┘         └──┘  └───┘  
src                         └──┘  └───┘           └──┘  └───┘          └───┘
typ                        └──┘  └───┘         └──┘  └───┘        └───┘
doc                                                                       └───┘
txt                                                                       └───┘
par                                                                       └───┘
pid                                                                           
st                                                                       └────┘
206  
207  /-- An inner product space forms a normed space over reals w.r.t. its associated norm. -/
208  instance inner_product_space_is_normed_space : normed_space ℝ α :=
id                                                  └──────────┘  
src                                                 └──────────┘ 
typ                                                 └──────────┘  
doc                                                 └──────────┘
209  { norm_smul := assume r x,
id                          
typ                         
210    begin
st     └─────
211      rw [norm_eq_sqrt_inner, sqrt_eq_iff_mul_self_eq,
id           └────────────────┘  └─────────────────────┘
src      └──┘└────────────────┘└┘└─────────────────────┘└─
typ      └──┘└────────────────┘└┘└─────────────────────┘└─
doc      └──┘                  └┘                       └─
txt      └──┘                  └┘                       └─
par      └──┘                  └┘                       └─
pid        └┘                  └┘                       └─
st   ─────────────────────────┘└───────────────────────┘└─
212          inner_smul_left, inner_smul_right, inner_self_eq_norm_square],
id           └─────────────┘  └──────────────┘  └───────────────────────┘
src  ───────┘└─────────────┘└┘└──────────────┘└┘└───────────────────────┘
typ  ───────┘└─────────────┘└┘└──────────────┘└┘└───────────────────────┘
doc  ───────┘               └┘                └┘                         
txt  ───────┘               └┘                └┘                         
par  ───────┘               └┘                └┘                         
pid  ───────┘               └┘                └┘                         
st   ──────────────────────┘└────────────────┘└─────────────────────────┘└──
213      exact calc
src      └────┘    
typ      └────┘    
doc      └────┘    
txt      └────┘    
par      └────┘    
pid               
st   ───────────────
214        abs(r) * ∥x∥ * (abs(r) * ∥x∥) = (abs(r) * abs(r)) * (∥x∥ * ∥x∥) : by ring
id                                                └─┘
src  ─────┘     └┘        └┘    └┘       └┘ └─┘  └─┘         └──┘  └────
typ  ─────┘     └┘        └┘    └┘       └┘ └─┘  └─┘         └──┘  └────
doc  ─────┘     └┘           └┘    └┘       └┘      └─┘         └──┘  └────
txt  ─────┘     └┘           └┘    └┘       └┘      └─┘         └──┘  └────
par  ─────┘     └┘           └┘    └┘       └┘      └─┘         └──┘  └────
pid  ─────┘     └┘           └┘    └┘       └┘      └─┘         └──┘  └─────
st   ─────────────────────────────────────────────────────────────────────────┘└─────
215        ... = r * (r * (∥x∥ * ∥x∥)) : by { rw abs_mul_abs_self, ring },
id                                             └──────────────┘
src  ─────┘└──┘              └───┘  └─┘└─┘└──────────────┘└┘└───┘
typ  ─────┘└──┘            └───┘  └─┘└─┘└──────────────┘└┘└───┘
doc  ─────┘└──┘              └───┘  └─┘└─┘                └┘└───┘
txt  ─────┘└──┘              └───┘  └─┘└─┘                └┘└───┘
par  ─────┘└──┘              └───┘  └─┘└─┘                └┘└───┘
pid  ─────────┘              └───┘  └────┘                └──────┘
st   ─────┘└──────────────────────────────┘└────────────────────┘└─────┘└┘
216      exact inner_self_nonneg,
id             └───────────────┘
src      └────┘└───────────────┘
typ      └────┘└───────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────┘└─
217      exact mul_nonneg (abs_nonneg _) (sqrt_nonneg _)
id             └────────┘  └────────┘     └─────────┘
src      └────┘└────────┘ └────────┘└──┘ └─────────┘└───
typ      └────┘└────────┘ └────────┘└──┘ └─────────┘└───
doc      └────┘                     └──┘            └───
txt      └────┘                     └──┘            └───
par      └────┘                     └──┘            └───
pid                                └──┘            └─┘
st   ────────────────────────────────────────────────────
218    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
219  
220  end norm
221  
222  section orthogonal
223  
224  open filter
225  
226  /--
227  Existence of minimizers
228  Let `u` be a point in an inner product space, and let `K` be a nonempty complete convex subset.
229  Then there exists a unique `v` in `K` that minimizes the distance `∥u - v∥` to `u`.
230   -/
231  theorem exists_norm_eq_infi_of_complete_convex {K : set α} (ne : K.nonempty) (h₁ : is_complete K)
id                                                       └─┘         └───────┘        └─────────┘ 
src                                                      └─┘           └───────┘        └─────────┘
typ                                                      └─┘         └───────┘        └─────────┘ 
doc                                                                    └───────┘        └─────────┘
232    (h₂ : convex K) : ∀ u : α, ∃ v ∈ K, ∥u - v∥ = ⨅ w : K, ∥u - w∥ := assume u,
id           └────┘                                         
src          └────┘                                       
typ          └────┘                                         
doc          └────┘                                        
233  begin
st   └─────
234    let δ := ⨅ w : K, ∥u - w∥,
id                       
src    └───────┘└───┘   
typ    └───────┘└───┘ 
doc    └───────┘└───┘    
txt    └───────┘ └───┘     
par    └───────┘ └───┘     
pid    └───┘└─┘ └───┘     
st   ──────────────────────────┘└─
235    letI : nonempty K := ne.to_subtype,
id            └──────┘     └───────────┘
src    └─────┘└──────┘ └──┘└───────────┘
typ    └─────┘└──────┘└──┘└───────────┘
doc    └─────┘         └──┘
txt    └─────┘         └──┘
par    └─────┘         └──┘
pid        └┘         └──┘
st   ───────────────────────────────────┘└─
236    have zero_le_δ : 0 ≤ δ,
id                         
src    └─────────────────┘
typ    └─────────────────┘
doc    └─────────────────┘ 
txt    └─────────────────┘ 
par    └─────────────────┘ 
pid    └────────────┘└───┘ 
st   ───────────────────────┘└─
237      apply le_cinfi, intro, exact norm_nonneg _,
id             └──────┘               └─────────┘
src      └────┘└──────┘  └───┘  └────┘└─────────┘└┘
typ      └────┘└──────┘  └───┘  └────┘└─────────┘└┘
doc      └────┘└──────┘  └───┘  └────┘           └┘
txt      └────┘          └───┘  └────┘           └┘
par      └────┘          └───┘  └────┘           └┘
pid                                            └┘
st   ─────────────────┘└─────┘└───────────────────┘└─
238    have δ_le : ∀ w : K, δ ≤ ∥u - w∥,
id                             
src    └──────────┘ └───┘       
typ    └──────────┘ └───┘    
doc    └──────────┘ └───┘       
txt    └──────────┘ └───┘       
par    └──────────┘ └───┘       
pid    └───────┘└─┘ └───┘       
st   ─────────────────────────────────┘└─
239      assume w, apply cinfi_le, use (0:ℝ), rintros _ ⟨_, rfl⟩, exact norm_nonneg _,
id                       └──────┘                                       └─────────┘
src      └──────┘  └────┘└──────┘  └──┘ └┘   └────────────────┘  └────┘└─────────┘└┘
typ      └──────┘  └────┘└──────┘  └──┘ └┘   └────────────────┘  └────┘└─────────┘└┘
doc      └──────┘  └────┘└──────┘  └──┘ └┘   └────────────────┘  └────┘           └┘
txt      └──────┘  └────┘          └──┘ └┘   └────────────────┘  └────┘           └┘
par      └──────┘  └────┘          └──┘ └┘   └────────────────┘  └────┘           └┘
pid      └──────┘                     └┘          └─────────┘                  └┘
st   ───────────┘└──────────────┘└─────────┘└──────────────────┘└───────────────────┘└─
240    have δ_le' : ∀ w ∈ K, δ ≤ ∥u - w∥ := assume w hw, δ_le ⟨w, hw⟩,
id                                                    └──┘
src    └───────────┘ └───┘         └──┘      └─────┘      └┘  
typ    └───────────┘ └───┘      └──┘      └─────┘└──┘  └┘  
doc    └───────────┘ └───┘         └──┘      └─────┘      └┘  
txt    └───────────┘ └───┘         └──┘      └─────┘      └┘  
par    └───────────┘ └───┘         └──┘      └─────┘      └┘  
pid    └────────┘└─┘ └───┘         └──┘      └─────┘      └┘  
st   ───────────────────────────────────────────────────────────────┘└─
241    -- Step 1: since `δ` is the infimum, can find a sequence `w : ℕ → K` in `K`
st   ──────────────────────────────────────────────────────────────────────────────
242    -- such that `∥u - w n∥ < δ + 1 / (n + 1)` (which implies `∥u - w n∥ --> δ`);
st   ────────────────────────────────────────────────────────────────────────────────
243    -- maybe this should be a separate lemma
st   ───────────────────────────────────────────
244    have exists_seq : ∃ w : ℕ → K, ∀ n, ∥u - w n∥ < δ + 1 / (n + 1),
id                                                   
src    └────────────────┘└───┘    └┘        └─┘   └─┘
typ    └────────────────┘└───┘  └┘      └─┘   └─┘
doc    └────────────────┘ └───┘     └┘          └─┘    └─┘
txt    └────────────────┘ └───┘     └┘          └─┘    └─┘
par    └────────────────┘ └───┘     └┘          └─┘    └─┘
pid    └─────────────┘└─┘ └───┘     └┘          └─┘    └─┘
st   ────────────────────────────────────────────────────────────────┘└─
245      have hδ : ∀n:ℕ, δ < δ + 1 / (n + 1), from
id                           
src      └────────┘ └┘      └─┘    └─┘  └────
typ      └────────┘ └┘     └─┘    └─┘  └────
doc      └────────┘ └┘      └─┘    └─┘  └────
txt      └────────┘ └┘      └─┘    └─┘  └────
par      └────────┘ └┘      └─┘    └─┘  └────
pid      └─────┘└─┘ └┘      └─┘    └─┘  └────
st   ──────────────────────────────────────┘└──────
246        λ n, lt_add_of_le_of_pos (le_refl _) nat.one_div_pos_of_nat,
id              └─────────────────┘  └─────┘    └────────────────────┘
src  ─────┘ └──┘└─────────────────┘ └─────┘└──┘└────────────────────┘
typ  ─────┘ └──┘└─────────────────┘ └─────┘└──┘└────────────────────┘
doc  ─────┘ └──┘                           └──┘
txt  ─────┘ └──┘                           └──┘
par  ─────┘ └──┘                           └──┘
pid  ─────┘ └──┘                           └──┘
st   ────────────────────────────────────────────────────────────────┘└─
247      have h := λ n, exists_lt_of_cinfi_lt (hδ n),
id                      └───────────────────┘  └┘
src      └────────┘ └──┘└───────────────────┘    
typ      └────────┘ └──┘└───────────────────┘ └┘ 
doc      └────────┘ └──┘└───────────────────┘    
txt      └────────┘ └──┘                         
par      └────────┘ └──┘                         
pid      └────┘└─┘ └──┘                         
st   ──────────────────────────────────────────────┘└─
248      let w : ℕ → K := λ n, classical.some (h n),
id                            └────────────┘  
src      └──────┘   └──┘ └──┘└────────────┘   
typ      └──────┘  └──┘ └──┘└────────────┘  
doc      └──────┘   └──┘ └──┘                 
txt      └──────┘   └──┘ └──┘                 
par      └──────┘   └──┘ └──┘                 
pid      └───┘└─┘   └──┘ └──┘                 
st   ─────────────────────────────────────────────┘└─
249      exact ⟨w, λ n, classical.some_spec (h n)⟩,
id                     └─────────────────┘  
src      └────┘  └┘ └──┘└─────────────────┘   └┘
typ      └────┘ └┘ └──┘└─────────────────┘  └┘
doc      └────┘  └┘ └──┘                      └┘
txt      └────┘  └┘ └──┘                      └┘
par      └────┘  └┘ └──┘                      └┘
pid             └┘ └──┘                      └┘
st   ────────────────────────────────────────────┘└─
250    rcases exists_seq with ⟨w, hw⟩,
id            └────────┘
src    └─────┘          └───────────┘
typ    └─────┘└────────┘└───────────┘
doc    └─────┘          └───────────┘
txt    └─────┘          └───────────┘
par    └─────┘          └───────────┘
pid                    └───────────┘
st   ───────────────────────────────┘└─
251    have norm_tendsto : tendsto (λ n, ∥u - w n∥) at_top (𝓝 δ),
id                         └─────┘                └────┘   
src    └──────────────────┘└─────┘  └──┘      └┘└────┘  
typ    └──────────────────┘└─────┘  └──┘    └┘└────┘ 
doc    └──────────────────┘└─────┘  └──┘      └┘└────┘  
txt    └──────────────────┘         └──┘      └┘         
par    └──────────────────┘         └──┘      └┘         
pid    └───────────────┘└─┘         └──┘      └┘         
st   ──────────────────────────────────────────────────────────┘└─
252      have h : tendsto (λ n:ℕ, δ) at_top (𝓝 δ),
id                └─────┘            └────┘    
src      └───────┘└─────┘  └─┘ └┘ └┘└────┘   
typ      └───────┘└─────┘  └─┘ └┘ └┘└────┘  
doc      └───────┘└─────┘  └─┘ └┘ └┘└────┘   
txt      └───────┘         └─┘ └┘ └┘         
par      └───────┘         └─┘ └┘ └┘         
pid      └────┘└─┘         └─┘ └┘ └┘         
st   ───────────────────────────────────────────┘└─
253        exact tendsto_const_nhds,
id               └────────────────┘
src        └────┘└────────────────┘
typ        └────┘└────────────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────────────────────┘└─
254      have h' : tendsto (λ n:ℕ, δ + 1 / (n + 1)) at_top (𝓝 δ),
id                 └─────┘                          └────┘    
src      └────────┘└─────┘  └─┘ └┘  └─┘    └───┘└────┘   
typ      └────────┘└─────┘  └─┘ └┘  └─┘    └───┘└────┘  
doc      └────────┘└─────┘  └─┘ └┘  └─┘    └───┘└────┘   
txt      └────────┘         └─┘ └┘  └─┘    └───┘         
par      └────────┘         └─┘ └┘  └─┘    └───┘         
pid      └─────┘└─┘         └─┘ └┘  └─┘    └───┘         
st   ──────────────────────────────────────────────────────────┘└─
255        convert h.add tendsto_one_div_add_at_top_nhds_0_nat, simp only [add_zero],
id                 └───┘ └───────────────────────────────────┘             └──────┘
src        └──────┘└───┘└───────────────────────────────────┘  └─────────┘└──────┘
typ        └──────┘└───┘└───────────────────────────────────┘  └─────────┘└──────┘
doc        └──────┘                                            └─────────┘        
txt        └──────┘                                            └─────────┘        
par        └──────┘                                            └─────────┘        
pid                                                               └──┘└┘        
st   ────────────────────────────────────────────────────────┘└────────────────────┘└─
256      exact tendsto_of_tendsto_of_tendsto_of_le_of_le h h'
id             └───────────────────────────────────────┘  └┘
src      └────┘└───────────────────────────────────────┘   
typ      └────┘└───────────────────────────────────────┘└┘
doc      └────┘└───────────────────────────────────────┘   
txt      └────┘                                            
par      └────┘                                            
pid                                                       
st   ─────────────────────────────────────────────────────────
257        (filter.eventually_of_forall _ $ λ x, δ_le _)
id                                               └──┘
src  ─────┘                            └─┘  └──┘    └───
typ  ─────┘                            └─┘  └──┘└──┘└───
doc  ─────┘                            └─┘  └──┘    └───
txt  ─────┘                            └─┘  └──┘    └───
par  ─────┘                            └─┘  └──┘    └───
pid  ─────┘                            └─┘  └──┘    └───
st   ────────────────────────────────────────────────────
258        (filter.eventually_of_forall _ $ λ x, le_of_lt (hw _)),
id          └─────────────────────────┘          └──────┘  └┘
src  ─────┘ └─────────────────────────┘└─┘  └──┘└──────┘   └──┘
typ  ─────┘ └─────────────────────────┘└─┘  └──┘└──────┘ └┘└──┘
doc  ─────┘                            └─┘  └──┘           └──┘
txt  ─────┘                            └─┘  └──┘           └──┘
par  ─────┘                            └─┘  └──┘           └──┘
pid  ─────┘                            └─┘  └──┘           └──┘
st   ───────────────────────────────────────────────────────────┘└─
259    -- Step 2: Prove that the sequence `w : ℕ → K` is a Cauchy sequence
st   ──────────────────────────────────────────────────────────────────────
260    have seq_is_cauchy : cauchy_seq (λ n, ((w n):α)),
id                          └────────┘             
src    └───────────────────┘└────────┘  └──┘    └┘ └┘
typ    └───────────────────┘└────────┘  └──┘   └┘└┘
doc    └───────────────────┘└────────┘  └──┘    └┘ └┘
txt    └───────────────────┘            └──┘    └┘ └┘
par    └───────────────────┘            └──┘    └┘ └┘
pid    └────────────────┘└─┘            └──┘    └┘ └┘
st   ─────────────────────────────────────────────────┘└─
261      rw cauchy_seq_iff_le_tendsto_0, -- splits into three goals
id          └─────────────────────────┘
src      └─┘└─────────────────────────┘
typ      └─┘└─────────────────────────┘
doc      └─┘└─────────────────────────┘
txt      └─┘
par      └─┘
pid        
st   ─────────────────────────────────┘└────────────────────────────
262      let b := λ n:ℕ, (8 * δ * (1/(n+1)) + 4 * (1/(n+1)) * (1/(n+1))),
id                           
src      └───────┘ └─┘ └┘ └┘       └──┘ └─┘      └──┘      └──┘
typ      └───────┘ └─┘ └┘ └┘      └──┘ └─┘      └──┘      └──┘
doc      └───────┘ └─┘ └┘ └┘        └──┘ └─┘      └──┘      └──┘
txt      └───────┘ └─┘ └┘ └┘        └──┘ └─┘      └──┘      └──┘
par      └───────┘ └─┘ └┘ └┘        └──┘ └─┘      └──┘      └──┘
pid      └───┘└─┘ └─┘ └┘ └┘        └──┘ └─┘      └──┘      └──┘
st   ──────────────────────────────────────────────────────────────────┘└─
263      use (λn, sqrt (b n)),
id                └──┘  
src      └──┘  └─┘└──┘   └┘
typ      └──┘  └─┘└──┘  └┘
doc      └──┘  └─┘       └┘
txt      └──┘  └─┘       └┘
par      └──┘  └─┘       └┘
pid           └─┘       └┘
st   ───────────────────────┘└─
264      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
265      -- first goal :  `∀ (n : ℕ), 0 ≤ sqrt (b n)`
st   ─────────────────────────────────────────────────
266      assume n, exact sqrt_nonneg _,
id                       └─────────┘
src      └──────┘  └────┘└─────────┘└┘
typ      └──────┘  └────┘└─────────┘└┘
doc      └──────┘  └────┘           └┘
txt      └──────┘  └────┘           └┘
par      └──────┘  └────┘           └┘
pid      └──────┘                  └┘
st   ───────────┘└───────────────────┘└─
267      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
268      -- second goal : `∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ↑(w n) ↑(w m) ≤ sqrt (b N)`
st   ──────────────────────────────────────────────────────────────────────────────────────
269      assume p q N hp hq,
src      └────────────────┘
typ      └────────────────┘
doc      └────────────────┘
txt      └────────────────┘
par      └────────────────┘
pid      └────────────────┘
st   ─────────────────────┘└─
270      let wp := ((w p):α), let wq := ((w q):α),
id                                        
src      └────────┘    └┘   └────────┘    └┘ 
typ      └────────┘  └┘  └────────┘  └┘
doc      └────────┘    └┘   └────────┘    └┘ 
txt      └────────┘    └┘   └────────┘    └┘ 
par      └────────┘    └┘   └────────┘    └┘ 
pid      └────┘└─┘    └┘   └────┘└─┘    └┘ 
st   ──────────────────────┘└───────────────────┘└─
271      let a := u - wq, let b := u - wp,
id                   └┘              └┘
src      └───────┘      └───────┘  
typ      └───────┘ └┘  └───────┘ └┘
doc      └───────┘      └───────┘  
txt      └───────┘      └───────┘  
par      └───────┘      └───────┘  
pid      └───┘└─┘      └───┘└─┘  
st   ──────────────────┘└───────────────┘└─
272      let half := 1 / (2:ℝ), let div := 1 / ((N:ℝ) + 1),
id                                               
src      └────────────┘  └┘   └───────────┘     └┘ └─┘
typ      └────────────┘  └┘   └───────────┘    └┘ └─┘
doc      └────────────┘  └┘   └───────────┘     └┘ └─┘
txt      └────────────┘  └┘   └───────────┘     └┘ └─┘
par      └────────────┘  └┘   └───────────┘     └┘ └─┘
pid      └──────┘└───┘  └┘   └─────┘└───┘     └┘ └─┘
st   ────────────────────────┘└──────────────────────────┘└─
273      have : 4 * ∥u - half • (wq + wp)∥ * ∥u - half • (wq + wp)∥ + ∥wp - wq∥ * ∥wp - wq∥ =
id                                              └──┘                             └┘   └┘  
src      └───────┘                                               
typ      └───────┘                  └──┘                  └┘ └┘ 
doc      └───────┘                                                 
txt      └───────┘                                                 
par      └───────┘                                                 
pid      └───┘└──┘                                                 
st   ─────────────────────────────────────────────────────────────────────────────────────────
274        2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) :=
id                                
src  ───────┘                 └────
typ  ───────┘               └────
doc  ───────┘                 └────
txt  ───────┘                 └────
par  ───────┘                 └────
pid  ───────┘                 └───
st   ─────────────────────────────────────
275      calc
src  ───┘    
typ  ───┘    
doc  ───┘    
txt  ───┘    
par  ───┘    
pid  ───┘    
st   ─────────
276        4 * ∥u - half•(wq + wp)∥ * ∥u - half•(wq + wp)∥ + ∥wp - wq∥ * ∥wp - wq∥
src  ───────┘                                                
typ  ───────┘                                                
doc  ───────┘                                                
txt  ───────┘                                                
par  ───────┘                                                
pid  ───────┘                                                
st   ──────────────────────────────────────────────────────────────────────────────
277            = (2*∥u - half•(wq + wp)∥) * (2 * ∥u - half•(wq + wp)∥) + ∥wp-wq∥*∥wp-wq∥ : by ring
id                                                   └──┘                        └┘ └┘
src  ─────────┘                  └┘  └┘                └┘                └─┘  └────
typ  ─────────┘                  └┘  └┘   └──┘        └┘          └┘ └┘ └─┘  └────
doc  ─────────┘                  └┘  └┘                └┘                └─┘  └────
txt  ─────────┘                  └┘  └┘                └┘                └─┘  └────
par  ─────────┘                  └┘  └┘                └┘                └─┘  └────
pid  ─────────┘                  └┘  └┘                └┘                └─┘  └─────
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─────
278        ... = (abs((2:ℝ)) * ∥u - half•(wq + wp)∥) * (abs((2:ℝ)) * ∥u - half•(wq+wp)∥) + ∥wp-wq∥*∥wp-wq∥ :
id                                                      └─┘
src  ─────┘└──┘       └┘ └─┘                └┘  └─┘  └┘ └─┘                └┘                └──
typ  ─────┘└──┘       └┘ └─┘                └┘  └─┘  └┘ └─┘                └┘                └──
doc  ─────┘└──┘       └┘ └─┘                └┘       └┘ └─┘                └┘                └──
txt  ─────┘└──┘       └┘ └─┘                └┘       └┘ └─┘                └┘                └──
par  ─────┘└──┘       └┘ └─┘                └┘       └┘ └─┘                └┘                └──
pid  ─────────┘       └┘ └─┘                └┘       └┘ └─┘                └┘                └──
st   ─────┘└─────────────────────────────────────────────────────────────────────────────────────────────────
279        by { rw abs_of_nonneg, exact add_nonneg zero_le_one zero_le_one }
id                 └───────────┘        └────────┘             └─────────┘
src  ─────┘  └─┘└─┘└───────────┘└┘└────┘└────────┘           └─────────┘└─
typ  ─────┘  └─┘└─┘└───────────┘└┘└────┘└────────┘           └─────────┘└─
doc  ─────┘  └─┘└─┘             └┘└────┘                                └─
txt  ─────┘  └─┘└─┘             └┘└────┘                                └─
par  ─────┘  └─┘└─┘             └┘└────┘                                └─
pid  ─────┘  └────┘             └──────┘                                └──
st   ───────┘└─────────────────┘└─────────────────────────────────────────┘
280        ... = ∥(2:ℝ) • (u - half • (wq + wp))∥ * ∥(2:ℝ) • (u - half • (wq + wp))∥ + ∥wp-wq∥ * ∥wp-wq∥ :
src  ─────────┘   └┘ └┘               └┘    └┘ └┘               └┘                 └──
typ  ─────────┘   └┘ └┘               └┘    └┘ └┘               └┘                 └──
doc  ─────────┘   └┘ └┘               └┘    └┘ └┘               └┘                 └──
txt  ─────────┘   └┘ └┘               └┘    └┘ └┘               └┘                 └──
par  ─────────┘   └┘ └┘               └┘    └┘ └┘               └┘                 └──
pid  ─────────┘   └┘ └┘               └┘    └┘ └┘               └┘                 └──
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────
281          by { rw [norm_smul], refl }
id                    └───────┘
src  ───────┘  └─┘└──┘└───────┘└┘└───┘└─
typ  ───────┘  └─┘└──┘└───────┘└┘└───┘└─
doc  ───────┘  └─┘└──┘         └┘└───┘└─
txt  ───────┘  └─┘└──┘         └┘└───┘└─
par  ───────┘  └─┘└──┘         └┘└───┘└─
pid  ───────┘  └─────┘         └─────────
st   ─────────┘└──────────────┘└──────┘
282        ... = ∥a + b∥ * ∥a + b∥ + ∥a - b∥ * ∥a - b∥ :
src  ─────────┘                        └──
typ  ─────────┘                        └──
doc  ─────────┘                        └──
txt  ─────────┘                        └──
par  ─────────┘                        └──
pid  ─────────┘                        └──
st   ────────────────────────────────────────────────────
283        begin
src  ─────┘     
typ  ─────┘     
doc  ─────┘     
txt  ─────┘     
par  ─────┘     
pid  ─────┘     
st   ─────┘└─────
284          rw [smul_sub, smul_smul, mul_one_div_cancel two_ne_zero, ← one_add_one_eq_two, add_smul],
id               └──────┘  └───────┘  └────────────────┘ └─────────┘    └────────────────┘  └──────┘
src  ───────┘└──┘└──────┘└┘└───────┘└┘└────────────────┘└─────────┘└──┘└────────────────┘└┘└──────┘└─
typ  ───────┘└──┘└──────┘└┘└───────┘└┘└────────────────┘└─────────┘└──┘└────────────────┘└┘└──────┘└─
doc  ───────┘└──┘        └┘         └┘                             └──┘                  └┘        └─
txt  ───────┘└──┘        └┘         └┘                             └──┘                  └┘        └─
par  ───────┘└──┘        └┘         └┘                             └──┘                  └┘        └─
pid  ───────────┘        └┘         └┘                             └──┘                  └┘        └──
st   ───────────────────┘└─────────┘└──────────────────────────────┘└────────────────────┘└────────┘└──
285          simp only [one_smul],
id                      └──────┘
src  ───────┘└─────────┘└──────┘└─
typ  ───────┘└─────────┘└──────┘└─
doc  ───────┘└─────────┘        └─
txt  ───────┘└─────────┘        └─
par  ───────┘└─────────┘        └─
pid  ──────────────────┘        └──
st   ───────────────────────────┘└─
286          have eq₁ : wp - wq = a - b, show wp - wq = (u - wq) - (u - wp), abel,
id                      └┘   └┘                            └┘        └┘
src  ──────────────────┘         └┘└───┘           └┘      └┘└──┘└─
typ  ──────────────────┘└┘ └┘  └┘└───┘         └┘└┘   └┘└┘└──┘└─
doc  ──────────────────┘         └┘└───┘           └┘      └┘└──┘└─
txt  ──────────────────┘         └┘└───┘           └┘      └┘└──┘└─
par  ──────────────────┘         └┘└───┘           └┘      └┘└──┘└─
pid  ──────────────────┘         └─────┘           └┘      └────────
st   ─────────────────────────────────┘└──────────────────────────────────┘└────┘└─
287          have eq₂ : u + u - (wq + wp) = a + b, show u + u - (wq + wp) = (u - wq) + (u - wp), abel,
id                              └┘   └┘                                       └┘        └┘
src  ──────────────────┘          └┘    └┘└───┘          └┘      └┘      └┘└──┘└─
typ  ──────────────────┘    └┘ └┘└┘  └┘└───┘          └┘    └┘└┘   └┘└┘└──┘└─
doc  ──────────────────┘          └┘    └┘└───┘          └┘      └┘      └┘└──┘└─
txt  ──────────────────┘          └┘    └┘└───┘          └┘      └┘      └┘└──┘└─
par  ──────────────────┘          └┘    └┘└───┘          └┘      └┘      └┘└──┘└─
pid  ──────────────────┘          └┘    └─────┘          └┘      └┘      └────────
st   ───────────────────────────────────────────┘└────────────────────────────────────────────┘└────┘└─
288          rw [eq₁, eq₂],
id               └─┘  └─┘
src  ───────┘└──┘   └┘   └─
typ  ───────┘└──┘└─┘└┘└─┘└─
doc  ───────┘└──┘   └┘   └─
txt  ───────┘└──┘   └┘   └─
par  ───────┘└──┘   └┘   └─
pid  ───────────┘   └┘   └──
st   ──────────────┘└───┘└──
289        end
src  ──────────
typ  ──────────
doc  ──────────
txt  ──────────
par  ──────────
pid  ──────────
st   ────────┘
290        ... = 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) : parallelogram_law_with_norm,
id                                           └─────────────────────────┘
src  ─────────┘ └─┘                 └──┘└─────────────────────────┘
typ  ─────────┘ └─┘               └──┘└─────────────────────────┘
doc  ─────────┘ └─┘                 └──┘
txt  ─────────┘ └─┘                 └──┘
par  ─────────┘ └─┘                 └──┘
pid  ─────────┘ └─┘                 └──┘
st   ────────────────────────────────────────────────────────────────────┘└─
291      have eq : δ ≤ ∥u - half • (wq + wp)∥,
id                        └──┘    └┘   └┘
src      └────────┘                
typ      └────────┘   └──┘  └┘ └┘
doc      └────────┘                
txt      └────────┘                
par      └────────┘                
pid      └─────┘└─┘                
st   ───────────────────────────────────────┘└─
292        rw smul_add,
id            └──────┘
src        └─┘└──────┘
typ        └─┘└──────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ────────────────┘└─
293        apply δ_le', apply h₂,
src        └────┘       └────┘
typ        └────┘       └────┘
doc        └────┘       └────┘
txt        └────┘       └────┘
par        └────┘       └────┘
pid                         
st   ────────────────┘└────────┘└─
294          repeat {exact subtype.mem _},
id                         └─────────┘
src          └──────┘└────┘└─────────┘└┘
typ          └──────┘└────┘└─────────┘└┘
doc          └──────┘└────┘           └┘
txt          └──────┘└────┘           └┘
par          └──────┘└────┘           └┘
pid                └──────┘           └─┘
st   ───────────────┘└─────────────────┘└┘
295          repeat {exact le_of_lt one_half_pos},
id                         └──────┘ └──────────┘
src          └──────┘└────┘└──────┘└──────────┘
typ          └──────┘└────┘└──────┘└──────────┘
doc          └──────┘└────┘                    
txt          └──────┘└────┘                    
par          └──────┘└────┘                    
pid                └──────┘                    
st   ───────────────┘└─────────────────────────┘└┘
296          exact add_halves 1,
id                 └────────┘
src          └────┘└────────┘└┘
typ          └────┘└────────┘└┘
doc          └────┘          └┘
txt          └────┘          └┘
par          └────┘          └┘
pid                         
st   ─────────────────────────┘└─
297      have eq₁ : 4 * δ * δ ≤ 4 * ∥u - half • (wq + wp)∥ * ∥u - half • (wq + wp)∥,
id                                                              └──┘    └┘   └┘
src      └───────────┘     └─┘                               
typ      └───────────┘    └─┘                   └──┘  └┘ └┘
doc      └───────────┘     └─┘                               
txt      └───────────┘     └─┘                               
par      └───────────┘     └─┘                               
pid      └──────┘└───┘     └─┘                               
st   ─────────────────────────────────────────────────────────────────────────────┘
298        mono, mono, norm_num, apply mul_nonneg, norm_num, exact norm_nonneg _,
299      have eq₂ : ∥a∥ * ∥a∥ ≤ (δ + div) * (δ + div) :=
id                                             └─┘
typ                                            └─┘
300        mul_self_le_mul_self (norm_nonneg _)
301          (le_trans (le_of_lt $ hw q) (add_le_add_left (nat.one_div_le_one_div hq) _)),
id                                                                               └┘
typ                                                                              └┘
302      have eq₂' : ∥b∥ * ∥b∥ ≤ (δ + div) * (δ + div) :=
id                                              └─┘
typ                                             └─┘
303        mul_self_le_mul_self (norm_nonneg _)
304          (le_trans (le_of_lt $ hw p) (add_le_add_left (nat.one_div_le_one_div hp) _)),
id                                                                               └┘
typ                                                                              └┘
305      rw dist_eq_norm,
306      apply nonneg_le_nonneg_of_squares_le, { exact sqrt_nonneg _ },
st                                                                   └┘
307      rw mul_self_sqrt,
308      exact calc
309        ∥wp - wq∥ * ∥wp - wq∥ = 2 * (∥a∥*∥a∥ + ∥b∥*∥b∥) - 4 * ∥u - half • (wq+wp)∥ * ∥u - half • (wq+wp)∥ :
id                                                                                        └──┘    └┘ └┘
typ                                                                                       └──┘    └┘ └┘
310          by { rw ← this, simp }
st                                └┘
311        ... ≤ 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) - 4 * δ * δ : sub_le_sub_left eq₁ _
id                                                     
typ                                                    
312        ... ≤ 2 * ((δ + div) * (δ + div) + (δ + div) * (δ + div)) - 4 * δ * δ :
313          sub_le_sub_right (mul_le_mul_of_nonneg_left (add_le_add eq₂ eq₂') (by norm_num)) _
314        ... = 8 * δ * div + 4 * div * div : by ring,
id                                       └─┘
typ                                      └─┘
315      exact add_nonneg (mul_nonneg (mul_nonneg (by norm_num) zero_le_δ) (le_of_lt nat.one_div_pos_of_nat))
316        (mul_nonneg (mul_nonneg (by norm_num) (le_of_lt nat.one_div_pos_of_nat)) (le_of_lt nat.one_div_pos_of_nat)),
317      -- third goal : `tendsto (λ (n : ℕ), sqrt (b n)) at_top (𝓝 0)`
318      apply tendsto.comp,
319      { convert continuous_sqrt.continuous_at, exact sqrt_zero.symm },
st                                                                     └┘
320      have eq₁ : tendsto (λ (n : ℕ), 8 * δ * (1 / (n + 1))) at_top (𝓝 (0:ℝ)),
id                                          
typ                                         
321        convert (@tendsto_const_nhds _ _ _ (8 * δ) _).mul tendsto_one_div_add_at_top_nhds_0_nat,
id                                                 
typ                                                
322        simp only [mul_zero],
323      have : tendsto (λ (n : ℕ), (4:ℝ) * (1 / (n + 1))) at_top (𝓝 (0:ℝ)),
324        convert (@tendsto_const_nhds _ _ _ (4:ℝ) _).mul tendsto_one_div_add_at_top_nhds_0_nat,
325        simp only [mul_zero],
326      have eq₂ : tendsto (λ (n : ℕ), (4:ℝ) * (1 / (n + 1)) * (1 / (n + 1))) at_top (𝓝 (0:ℝ)),
327        convert this.mul tendsto_one_div_add_at_top_nhds_0_nat,
328        simp only [mul_zero],
329      convert eq₁.add eq₂, simp only [add_zero],
330    -- Step 3: By completeness of `K`, let `w : ℕ → K` converge to some `v : K`.
331    -- Prove that it satisfies all requirements.
332    rcases cauchy_seq_tendsto_of_is_complete h₁ (λ n, _) seq_is_cauchy with ⟨v, hv, w_tendsto⟩,
id                                                    
typ                                                   
333    use v, use hv,
id         
typ        
334    have h_cont : continuous (λ v, ∥u - v∥) :=
id                                    
typ                                   
335      continuous.comp continuous_norm (continuous.sub continuous_const continuous_id),
336    have : tendsto (λ n, ∥u - w n∥) at_top (𝓝 ∥u - v∥),
id                                                  
typ                                                 
337      convert (tendsto.comp h_cont.continuous_at w_tendsto),
338    exact tendsto_nhds_unique at_top_ne_bot this norm_tendsto,
339    exact subtype.mem _
340  end
st   └─┘
341  
342  /-- Characterization of minimizers in the above theorem -/
343  theorem norm_eq_infi_iff_inner_le_zero {K : set α} (h : convex K) {u : α} {v : α}
id                                                                              
src                                                
typ                                                                             
344    (hv : v ∈ K) : ∥u - v∥ = (⨅ w : K, ∥u - w∥) ↔ ∀ w ∈ K, inner (u - v) (w - v) ≤ 0 :=
id                                                                     
src                                                
typ                                                                    
345  iff.intro
346  begin
347    assume eq w hw,
348    let δ := ⨅ w : K, ∥u - w∥, let p := inner (u - v) (w - v), let q := ∥w - v∥^2,
id                                                                         
typ                                                                        
349    letI : nonempty K := ⟨⟨v, hv⟩⟩,
id            └──────┘       
src           └──────┘
typ           └──────┘       
350    have zero_le_δ : 0 ≤ δ,
id                          
typ                         
351      apply le_cinfi, intro, exact norm_nonneg _,
352    have δ_le : ∀ w : K, δ ≤ ∥u - w∥,
id                              
typ                             
353      assume w, apply cinfi_le, use (0:ℝ), rintros _ ⟨_, rfl⟩, exact norm_nonneg _,
354    have δ_le' : ∀ w ∈ K, δ ≤ ∥u - w∥ := assume w hw, δ_le ⟨w, hw⟩,
id                                              
typ                                             
355    have : ∀θ:ℝ, 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q,
id                                             
typ                                            
356      assume θ hθ₁ hθ₂,
357      have : ∥u - v∥^2 ≤ ∥u - v∥^2 - 2 * θ * inner (u - v) (w - v) + θ*θ*∥w - v∥^2 :=
id                                                                            
typ                                                                           
358      calc
359        ∥u - v∥^2 ≤ ∥u - (θ•w + (1-θ)•v)∥^2 :
id                                    
typ                                   
360        begin
361          simp only [pow_two], apply mul_self_le_mul_self (norm_nonneg _),
362          rw [eq], apply δ_le',
363          apply h hw hv,
364          exacts [le_of_lt hθ₁, sub_nonneg.2 hθ₂, add_sub_cancel'_right _ _],
365        end
st         └─┘
366        ... = ∥(u - v) - θ • (w - v)∥^2 :
367        begin
368          have : u - (θ•w + (1-θ)•v) = (u - v) - θ • (w - v),
id                                                        
typ                                                       
369            rw [smul_sub, sub_smul, one_smul], simp,
370          rw this
371        end
st         └─┘
372        ... = ∥u - v∥^2 - 2 * θ * inner (u - v) (w - v) + θ*θ*∥w - v∥^2 :
373        begin
374          rw [norm_sub_pow_two, inner_smul_right, norm_smul],
375          simp only [pow_two],
376          show ∥u-v∥*∥u-v∥-2*(θ*inner(u-v)(w-v))+abs(θ)*∥w-v∥*(abs(θ)*∥w-v∥)=
377                  ∥u-v∥*∥u-v∥-2*θ*inner(u-v)(w-v)+θ*θ*(∥w-v∥*∥w-v∥),
id                                                              
typ                                                             
378          rw abs_of_pos hθ₁, ring
379        end,
st         └─┘
380      have eq₁ : ∥u-v∥^2-2*θ*inner(u-v)(w-v)+θ*θ*∥w-v∥^2=∥u-v∥^2+(θ*θ*∥w-v∥^2-2*θ*inner(u-v)(w-v)), abel,
id                                                                                             
typ                                                                                            
381      rw [eq₁, le_add_iff_nonneg_right] at this,
382      have eq₂ : θ*θ*∥w-v∥^2-2*θ*inner(u-v)(w-v)=θ*(θ*∥w-v∥^2-2*inner(u-v)(w-v)), ring,
id                                                                           
typ                                                                          
383      rw eq₂ at this,
384      have := le_of_sub_nonneg (nonneg_of_mul_nonneg_left this hθ₁),
385      exact this,
386    by_cases hq : q = 0,
id                   
typ                  
387    { rw hq at this,
388      have : p ≤ 0,
id              
typ             
389        have := this (1:ℝ) (by norm_num) (by norm_num),
390        linarith,
391      exact this },
st                  └┘
392    { have q_pos : 0 < q,
id                        
typ                       
393        apply lt_of_le_of_ne, exact pow_two_nonneg _, intro h, exact hq h.symm,
394      by_contradiction hp, rw not_le at hp,
395      let θ := min (1:ℝ) (p / q),
id                              
typ                             
396      have eq₁ : θ*q ≤ p := calc
id                      
typ                     
397        θ*q ≤ (p/q) * q : mul_le_mul_of_nonneg_right (min_le_right _ _) (pow_two_nonneg _)
id                      
typ                     
398        ... = p : div_mul_cancel _ hq,
id               
typ              
399      have : 2 * p ≤ p := calc
id                      
typ                     
400        2 * p ≤ θ*q : by { refine this θ (lt_min (by norm_num) (div_pos hp q_pos)) (by norm_num) }
id                                      
typ                                     
st                                                                                                  └┘
401        ... ≤ p : eq₁,
id               
typ              
402      linarith }
st                └─
403  end
st   ──┘
404  begin
405    assume h,
406    letI : nonempty K := ⟨⟨v, hv⟩⟩,
id            └──────┘       
src           └──────┘
typ           └──────┘       
407    apply le_antisymm,
408    { apply le_cinfi, assume w,
409      apply nonneg_le_nonneg_of_squares_le (norm_nonneg _),
410      have := h w w.2,
411      exact calc
412        ∥u - v∥ * ∥u - v∥ ≤ ∥u - v∥ * ∥u - v∥ - 2 * inner (u - v) ((w:α) - v) : by linarith
id                                                                          
typ                                                                         
413        ... ≤ ∥u - v∥^2 - 2 * inner (u - v) ((w:α) - v) + ∥(w:α) - v∥^2 :
414          by { rw pow_two, refine le_add_of_nonneg_right _, exact pow_two_nonneg _ }
st                                                                                    └┘
415        ... = ∥(u - v) - (w - v)∥^2 : norm_sub_pow_two.symm
416        ... = ∥u - w∥ * ∥u - w∥ :
417          by { have : (u - v) - (w - v) = u - w, abel, rw [this, pow_two] } },
id                                          
typ                                         
st                                                                          └──┘
418    { show (⨅ (w : K), ∥u - w∥) ≤ (λw:K, ∥u - w∥) ⟨v, hv⟩,
id                                                   
typ                                                  
419        apply cinfi_le, use 0, rintros y ⟨z, rfl⟩, exact norm_nonneg _ }
st                                                                        └─
420  end
st   ──┘
421  
422  /--
423  Existence of minimizers.
424  Let `u` be a point in an inner product space, and let `K` be a nonempty complete subspace.
425  Then there exists a unique `v` in `K` that minimizes the distance `∥u - v∥` to `u`.
426  This point `v` is usually called the orthogonal projection of `u` onto `K`.
427  -/
428  theorem exists_norm_eq_infi_of_complete_subspace (K : subspace ℝ α)
id                                                                   
src                                                                 
typ                                                                  
429    (h : is_complete (↑K : set α)) : ∀ u : α, ∃ v ∈ K, ∥u - v∥ = ⨅ w : (↑K : set α), ∥u - w∥ :=
id                            └┘                                                  
src                           └┘                                                 
typ                           └┘                                                  
430  exists_norm_eq_infi_of_complete_convex ⟨0, K.zero⟩ h K.convex
431  
432  /--
433  Characterization of minimizers in the above theorem.
434  Let `u` be a point in an inner product space, and let `K` be a nonempty subspace.
435  Then point `v` minimizes the distance `∥u - v∥` if and only if
436  for all `w ∈ K`, `inner (u - v) w = 0` (i.e., `u - v` is orthogonal to the subspace `K`)
437  -/
438  theorem norm_eq_infi_iff_inner_eq_zero (K : subspace ℝ α) {u : α} {v : α}
id                                                                       
src                                                       
typ                                                                      
439    (hv : v ∈ K) : ∥u - v∥ = (⨅ w : (↑K : set α), ∥u - w∥) ↔ ∀ w ∈ K, inner (u - v) w = 0 :=
id                                                                            
src                                                         
typ                                                                           
440  iff.intro
441  begin
442    assume h,
443    have h : ∀ w ∈ K, inner (u - v) (w - v) ≤ 0,
id                                         
typ                                        
444    { rwa [norm_eq_infi_iff_inner_le_zero] at h, exacts [K.convex, hv] },
st                                                                        └┘
445    assume w hw,
446    have le : inner (u - v) w ≤ 0,
id                           
typ                          
447      let w' := w + v,
id                    
typ                   
448      have : w' ∈ K := submodule.add_mem _ hw hv,
id              └┘
typ             └┘
449      have h₁ := h w' this,
id                    └┘
typ                   └┘
450      have h₂ : w' - v = w, simp only [add_neg_cancel_right, sub_eq_add_neg],
id                 └┘      
typ                └┘      
451      rw h₂ at h₁, exact h₁,
452    have ge : inner (u - v) w ≥ 0,
id                           
typ                          
453      let w'' := -w + v,
id                      
typ                     
454      have : w'' ∈ K := submodule.add_mem _ (submodule.neg_mem _ hw) hv,
id              └─┘
typ             └─┘
455      have h₁ := h w'' this,
id                    └─┘
typ                   └─┘
456      have h₂ : w'' - v = -w, simp only [neg_inj', add_neg_cancel_right, sub_eq_add_neg],
id                 └─┘       
typ                └─┘       
457      rw [h₂, inner_neg_right] at h₁,
458      linarith,
459      exact le_antisymm le ge
460  end
st   └─┘
461  begin
462    assume h,
463    have : ∀ w ∈ K, inner (u - v) (w - v) ≤ 0,
id                                      
typ                                     
464      assume w hw,
465      let w' := w - v,
id                    
typ                   
466      have : w' ∈ K := submodule.sub_mem _ hw hv,
id              └┘
typ             └┘
467      have h₁ := h w' this,
id                    └┘
typ                   └┘
468      exact le_of_eq h₁,
469    rwa norm_eq_infi_iff_inner_le_zero,
470    exacts [submodule.convex _, hv]
471  end
st   └─┘
472  
473  end orthogonal